<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/x
html1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type"
      content="text/html ; charset=US-ASCII" />
<title>Release Notes for Kananaskis-3 version of HOL 4</title>
</head>

<body>
<h1>Notes on HOL 4, Kananaskis-3 release</h1>

<h2 id="contents">Contents</h2>
<ul>
  <li> <a href="#new-features">New features</a> </li>
  <li> <a href="#bugs-fixed">Bugs fixed</a> </li>
  <li> <a href="#new-theories">New theories</a> </li>
  <li> <a href="#new-tools">New tools</a> </li>
  <li> <a href="#new-examples">New examples</a> </li>
  <li> <a href="#incompatibilities">Incompatibilities</a> </li>
</ul>



<h2 id="new-features">New features:</h2>

<ul>
<li> <p> Configuration and installation of the system is easier.
    Instead of having to edit <code>configure.sml</code> yourself,
    just pipe <code>tools/smart-configure</code> into
    <code>mosml</code> as the first step of installation (before
    build):</p>
<pre>
         mosml &lt; tools/smart-configure.sml
</pre></li>

<li> <p> The term and type parsers now report errors with an indication as
    to where in the parse they have occurred.  If the error is found
    during a run of Holmake, the location includes the line number in
    the file where the error is.  Pragma comments of the form
    <code>(*#loc&nbsp;100&nbsp;5*)</code> allow the line and column
    numbers to be overridden, &agrave; la C&rsquo;s <code>#line</code>
    directive.  (Many thanks to Keith Wansbrough for the
    implementation of this feature.)  The lexer is also much faster
    than it used to be.</p></li>

<li> <p> The system better distinguishes interactive and non-interactive
    use (the latter occurs with building things with Holmake).
    Diagnostic output is now rather different in non-interactive mode.
    Holmake comes with a new <code>-i</code> or
    <code>--interactive</code> flag to flip the underlying flag back
    to interactive, if you want to see "interactive mode" output.</p></li>

<li> <p> Holmake now supports the use of user-specified variables, in a
    manner analogous to that done by traditional make implementations.
    For example, one can define a variable <code>OBJS</code>,</p>

<pre>
         OBJS = foo bar baz
</pre>

    <p>and then refer to this variable elsewhere by writing
    <code>$(OBJS)</code> Holmake also provides some functions like
    those in GNU make for manipulating text (performing pattern-based
    substitutions, for example).  See the DESCRIPTION for more
    details. </p></li>

<li> <p> Performance when defining large record types (where the number of
    fields is greater than a user-adjustable reference variable), is
    now much improved.  Part of this change was to remove update
    functions as separate constants (they are now encoded using
    functional update functions), though the concrete syntax remains.
    See the DESCRIPTION for more details.</p></li>

<li> <p>In addition to the traditional $-prefix for making identifiers
    ignore their status as special forms in the grammar, HOL now
    supports the Caml method of enclosing identifiers in parentheses.
    Thus, instead of</p>
<pre>
         $/\ p
</pre>
    one can also write
<pre>
         (/\) p
</pre>

<p>    By default, the pretty-printer continues to print using the old
    $-syntax.  This can be changed by setting the trace variable
    <code>"pp_dollar_escapes"</code>.</p></li>



<li> <p> Pretty-printing of &ldquo;list forms&rdquo; (e.g., lists,
    sets and bags) is now under more user-control.  See the REFERENCE
    (or online help) for <code>add_listform</code>, whose type has
    changed, for more detail on this.  (Thanks to Lockwood Morris for
    this feature suggestion.)</p></li>

<li> <p>There are two new simpset fragments in realSimps.
    <code>REAL_REDUCE_ss</code>
    performs calculations over ground rational values.  Thus,</p>
<pre>
         SIMP_CONV (std_ss ++ REAL_REDUCE_ss) [] ``1/3 - 3/7``
</pre>
    returns
<pre>
         &gt; val it = |- 1 / 3 - 3 / 7 = ~2 / 21 : thm
</pre>

    <p>When <code>realSimps</code> is loaded, <code>REAL_REDUCE_ss</code>
    is automatically added to the stateful-rewriting simpset, and
    <code>bossLib</code>&rsquo;s <code>EVAL</code> is also augmented
    with this functionality.  This code also removes common factors
    from fractions even when there are no other arithmetic operations
    being performed.</p>

    <p> The second simpset fragment in <code>realSimps</code> is
    <code>REAL_ARITH_ss</code>, which embodies the
    <code>RealArith</code> decision procedure for universal Presburger
    arithmetic over the real numbers.</p></li>

<li> <p>The simplifier now provides simpler interfaces for the addition of
    AC-rewriting and congruence rules.  They can be added as if normal
    rewrites with the functions <code>simpLib.AC</code> and
    <code>simpLib.Cong</code>.  Thus,</p>
<pre>
         - SIMP_CONV bool_ss [AC ADD_COMM ADD_ASSOC] ``3 + x + y + 1``;
         &gt; val it = |- 3 + x + y + 1 = x + (y + (1 + 3)) : thm
</pre>
    <p><code>Cong</code> is used similarly.  Both functions are further
    described in the REFERENCE.</p></li>

<li> <p> Holmake now supports a new command-line option
    <code>--logging</code>, which tells it to record running times for
    the building of theories.  These times are stored in a file in the
    current directory.  See the DESCRIPTION for more
    details. </p></li>

<li> <p> Support for abbreviations in goals, via tactics such as
    <code>Q.ABBREV_TAC</code>, is now a deal richer.  Abbbreviations
    are now specially marked as such in a goal&rsquo;s assumptions,
    protecting them against being removed by tactics such as
    <code>RW_TAC</code> or <code>SRW_TAC</code>.  There are also new
    tactics for establishing abbreviations, such as
    <code>MATCH_ABBREV_TAC</code> and <code>PAT_ABBREV_TAC</code>.
    For more on these and other new tactics, see the REFERENCE (or the
    online help). </p>

    <p> To support old code, the old implementations of these tactics
    are available in a structure <code>OldAbbrevTactics</code>.  Thus,
    it is possible to restore a file to its old behaviour by
    including: </p>
<pre>
         structure Q = struct open Q open OldAbbrevTactics end;
</pre>
    <p> at the top of an affected file. </p> </li>

</ul>

<h2 id="bugs-fixed">Bugs fixed:</h2>

<ul>

  <li> <p><code>Hol_datatype</code> would fail if called on to define
      a type with a single nullary constructor.</p></li>

<li> <p><code>pred_setLib.UNION_CONV</code> (and other functions in this
    library) failed to work as advertised.  (Thanks to Lockwood Morris
    for the report of this bug.)</p></li>

<li> <p>It was too easy to do significant parser things before a
    <code>new_theory</code> declaration, causing these effects not to
    persist with the export of the theory.  Now, attempting to do this
    causes a strong warning to be issued.</p></li>

<li> <p><code>let</code> terms with bodies that were abstractions didn&rsquo;t
    print correctly.</p></li>

<li> <p>The type grammar didn&rsquo;t print stored type abbreviations
    correctly.</p></li>

<li> <p> Adding a user-supplied pretty-printer caused polymorphic terms to
    fail to print.  (The interface for adding pretty-printers is also
    now slightly richer, see the REFERENCE manual for details.)
    </p></li>

<li> <p><code>DECIDE_TAC</code> didn&rsquo;t pay attention to goal
    assumptions.</p></li>

<li> <p>A bug in <code>ARITH_CONV</code>&rsquo;s handling of conditional
    expressions caused some quantified goals to fail to be proved.</p></li>

<li> <p> The lexer got confused if a token made up of non-aggregating
    characters (e.g., including ";") was used, but not as part of
    special concrete syntax.  I.e., <code>;;</code> was OK as an
    infix, but not as a normal constant.  (Thanks to Klaus Schneider
    for the report of this bug.)</p></li>

<li> <p><code>SPEC_VAR</code> and theory export caused bound variables
    with the same name as constants to get changed.  (Thanks to
    Lockwood Morris for the report of this bug.)</p></li>

<li> <p> Many, many documentation typos and bugs were fixed.  (Thanks to
    Carl Witty for the report of most of these.)</p></li>

<li> <p> Two fixes for the simplifier&rsquo;s implementation of congruence rules.
    With deep nesting, congruence rules could lead to an exponential
    increase in time taken.  Also, terms that included variables used
    in a rule&rsquo;s statement could cause the rule to fail to fire.</p></li>

<li> <p>The simplifier&rsquo;s AC-rewriting could cause it to go into an
    infinite loop.  While the new behaviour does AC-normalise
    everywhere (we hope!), it is not necessarily the same as the old
    behaviour on examples which used to work. (Thanks to Tobias Nipkow
    for useful discussion about this bug.)</p></li>

<li> <p> <code>pairLib.PAIRED_ETA_CONV</code> was broken.  Thanks to
    Viktor Sabelfeld for the bug report.</p> </li>

<li> <p> <code>Q.UNDISCH_THEN</code> was behaving more as if it were
    <code>Q.PAT_UNDISCH_THEN</code>; it was finding matches in the
    assumptions rather than equal terms.  Thanks to Lockwood Morris
    for the bug report. </p> </li>

<li> <p> The order in which type arguments appeared as arguments to
    polymorphic type operators defined by <code>Hol_datatype</code>
    was previously undefined.  For example, if one wrote:</p>
<pre>
         Hol_datatype `sum = left of 'a | right of 'b`;
</pre>
    <p> it was not specified that <code>('a,'b)sum</code> was the type
    which associated the variable <code>'a</code> with the
    <code>left</code> constructor.  Now, the type picks up the type
    variable arguments in <code>Hol_datatype</code> in alphabetical
    order.  <em>This may break code that relied on what was an
    unspecified behaviour.</em></p></li>

<li><p> The quotation filter didn&rsquo;t recognise text of the form</p>
<pre>
         ``:
             foo
         ``
</pre>
    <p> with a newline immediately following the colon as a type
    quotation.   (Thanks to Steve Brackin for the report of this bug.)
    </p>
</li>


</ul>


<h2 id="new-theories">New theories:</h2>
<ul>
<li> <p> A theory of co-inductive (possibly infinite) labelled transition
    paths in <code>pathTheory</code>. </p> </li>
<li> <p> A theory of sorting and list permutations in
    <code>sortingTheory</code>. </p> </li>
</ul>

<h2 id="new-tools">New tools:</h2>

<ul>

  <li> <p> A new first-order proof tactic (called
      <code>METIS_TAC</code>) that uses ordered resolution and
      paramodulation, specifically tailored for subgoals that require
      equality reasoning.</p></li>

<li> <p> A &lsquo;boolification&rsquo; tool that automatically defines
    functions that map datatypes to boolean vectors. These kind of
    functions are needed for sending HOL subgoals to a model-checker
    or SAT solver.</p></li>
</ul>

<h2 id="new-examples">New examples:</h2>
<ul>
<li> <p> An extension of the existing lambda calculus example
    (examples/lambda) to include mechanisations of chapters&nbsp;2 &amp; 3 of
    Hankin&rsquo;s lambda calculus text, and the standardisation theorem
    from Barendregt&rsquo;s chapter&nbsp;11.</p></li>

<li> <p> A formalization of the probabilistic guarded command language
    (pGCL) in higher-order logic, including a tool for deriving
    sufficient verification conditions for partial correctness.</p></li>
</ul>

<h2 id="incompatibilities">Incompatibilities:</h2>

<ul> <li> <p> The four HOL executables have had their names adjusted.
We now think that using HOL with the quotation filter is the
appropriate default for all users.  To reflect this, the executable
<code>hol</code> now includes the quotation filter.  (This executable
used to be called <code>hol.unquote</code>.)  To avoid using the
quotation filter, use <code>hol.noquote</code>.  Analogous changes
have been made to <code>hol.bare</code>; <em>i.e.,</em>
<code>hol.bare</code> now includes the filter, and
<code>hol.bare.noquote</code> does not. </p></li>

<li> <p> The rewrite theorem for <code>LET</code>, </p>
<pre>
         LET f v = f v
</pre>
<p>    has been removed from <code>std_ss</code> and later simplification
    sets. (Simpsets <code>arith_ss</code>, <code>list_ss</code> and
    <code>srw_ss()</code> are all affected.)</p>
    <p> Old behaviours can be restored with code such as </p>
<pre>
         val std_ss = std_ss ++ simpLib.rewrites [LET_THM]
</pre>
</li>

<li> <p>Rewrite rules for <code>arithmeticTheory</code>&rsquo;s
    <code>MIN</code> and <code>MAX</code> constants have been made
    more general; they will now match more often.  For example,
    <code>MIN_LE</code> has changed from</p>
<pre>
         m &lt;= MIN m n = m &lt;= n
</pre>
    to
<pre>
         p &lt;= MIN m n = p &lt;= m /\ p &lt;= n
</pre></li>

<li> <p>For reasons of efficiency, all conversions in the system may now
    potentially raise the special exception
    <code>Conv.UNCHANGED</code> to indicate that they haven&rsquo;t changed
    the input term, and that they should be treated as if they had
    returned the theorem <code>|-&nbsp;t&nbsp;=&nbsp;t</code>, for
    input <code>t</code>.  Conversion connectives (such as
    <code>THENC</code>, <code>ORELSEC</code> and
    <code>TRY_CONV</code>) all do the appropriate thing in the
    presence of this exception.  Previously, sub-systems such as the
    simplifier, rewriter and arithmetic decision procedures have used
    this idea to make them work faster, but couldn&rsquo;t share information
    about unchangedness.</p>

<p> For interactive use, <code>CONV_RULE</code> and
    <code>CONV_TAC</code> handle the exception appropriately, and the
    new function <code>QCONV</code> (of type
    <code>:&nbsp;conv&nbsp;-&gt;&nbsp;conv</code>) can make any
    conversion handle <code>UNCHANGED</code>.  <code>QCONV</code>&rsquo;s
    implementation is</p>
<pre>
         fun QCONV c t = c t handle UNCHANGED => REFL t
</pre>

    If you have code implementing conversions of your own, you may
    need to fix code if it uses the following idiom:
<pre>
         fun myconv t =
           let val th = someconv t
               val ..  = &lt;fiddle with th&gt;
           in
               &lt;resulting theorem&gt;
           end
</pre>

    If <code>someconv</code> raises <code>UNCHANGED</code>, then
    <code>myconv</code> will too, causing expressions such as

<pre>
         myconv THENC &lt;something else&gt;
</pre>

    <p> to treat <code>myconv</code> as if it hadn&rsquo;t done anything
    (because the <code>&lt;fiddle&nbsp;with&nbsp;th&gt;</code> code
    never got called).</p>

    <p>This can be relatively difficult to track down, but the fix is
    simple enough: change <code>someconv&nbsp;t</code> to
    <code>QCONV&nbsp;someconv&nbsp;t</code>.</p></li>

<li> <p> The constant <code>LIST_TO_SET</code> is now defined in
    <code>listTheory</code>.</p></li>

<li> <p> The <code>word32</code> theory is not built by default.
    Instead, a general <code>word</code><em>n</em>-theory creating
    executable, <code>mkword.exe</code> is available in the
    <code>hol/bin/</code> directory.  This can be invoked to create
    word theories of various sizes.  For example,</p>
<pre>
         $ mkword.exe 32
</pre>
    <p> will create a <code>word32Theory</code> in the current
    directory.  These new theories don&rsquo;t have corresponding
    <code>Script</code> files, so <code>Holmake</code> doesn&rsquo;t
    automatically update these theories.  If this is a concern, the
    <code>Holmakefile</code> in
    <code>hol/src/n_bit/help/Holmakefile.example-32</code> demonstrates how to
    ensure word theories are rebuilt.</p></li>

<li> <p> The type <code>simpLib.ssdata</code> is now called
    <code>simpLib.ssfrag</code> and the constructor for this type that
    used to be called <code>SIMPSET</code> is now called
    <code>SSFRAG</code>.</p> </li>

</ul>


<hr />

<p> <em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-3</a></em> </p>

</body> </html>
